$M$.Msg $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Msg(($M$.2).1)